\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]$T$:Type.
\-\\[0ex]($\forall$$k$:Knd. ($k$ $\in$ ecl{-}trans{-}ks(ecl{-}trans($A$))) $\Rightarrow$ ($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ ($T$ = ecl{-}trans{-}type(ecl{-}trans($A$)))
\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](\=ecl{-}machine1\=\{ecl:ut2\}\+\+
\\[0ex]($i$; ${\it ds}$; ${\it da}$; $A$);
\-\\[0ex]ecl{-}machine3(\=${\it ds}$;\+
\\[0ex]${\it da}$;
\\[0ex]mkid\{ecl:ut2\};
\\[0ex]$T$;
\\[0ex]ecl{-}trans{-}ks(ecl{-}trans($A$));
\\[0ex]ecl{-}trans{-}a(ecl{-}trans($A$));
\\[0ex]${\it snd}$))
\-\-\-
\end{tabbing}